1. Technical Field
The present invention relates in general to logic network designs and in particular to the scalable reduction of logic network designs.
2. Description of the Related Art
Within the field of logic synthesis there is a major endeavor to minimize the cost necessary to implement logic networks. Many algorithms exist that are able to minimize the number of gates in the network. One example of theses algorithms is resubstitution. Resubstitution is an algorithm that is utilized to re-express functions in a logic design network in terms of other pre-existing functions. For example, within the Boolean functions F, G, and H, F may be expressed as F=func(G,H) for some function (func). The total cost to implement the network may be reduced as the gates implementing G and H can be repurposed to additionally implement F.
Traditionally resubstitution is performed using Binary Decision Diagrams (BDDs). However, BDDs do not scale well to industrial-sized logic networks, and therefore BDDs can only be used on very small logic networks. Resubstitution may also be performed utilizing a Boolean Satisfiability (SAT) solver. Incorporating a Boolean SAT solver scales much better than the use of BDDs, thereby suggesting that resubstitution may be able to scale to industrial-sized logic networks.
Formal verification is utilized to prove and/or disprove the properties of a logic network design. In the field of formal verification, or formal model checking, there exist several algorithms to prove temporal properties. Many of the algorithms utilized to prove temporal properties are not cost effective, and the computational complexity of the algorithms is proportional to the size of the logic network design, on which the algorithm operates.